Inference at * 1 
Iof proof for Lemma sub-equality:



1. T : Type
2. P : T
3. i : T
4. u : T
5. i = u
6. P(u)
  i = u 

latex

 by Assert P(i) 

latex

 1: .....assertion..... NILNIL

 1:   P(i)
 2: 

 2: 7. P(i)
 2:   i = u
 .

Definitions

f(a)